Nuprl Definition : es-local-prior-state 11,40

prior-state(f;base;X;e)
== if e  prior(X) then f(prior-state(f;base;X;prior(X)(e)),X(prior(X)(e))) else base fi 


clarification:

es-local-prior-state{i:l}
es-local-prior-state(es; f; base; X; e)
== if e  es-prior-interface{i:l}(es; X)
== then f
== then (es-local-prior-state{i:l}
== then (es-local-prior-state(es; f; base; X; es-prior-interface{i:l}(es; X)(e))
== then ,X(es-prior-interface{i:l}
== then ,X(es-prior-interface(es; X)(e)))
== else base
== fi 
(recursive) 
latex


Definitionsprior(X), X(e), f(a), e  X, if b then t else f fi , x.A(x), Y
FDL editor aliaseses-local-prior-state

origin